The present invention relates generally to tools that automatically verify, using static checking techniques, the correctness of a computer program with respect to predefined criteria, and particularly to a tool that derives verification conditions from a computer program source code. In particular, the present invention relates to the simplification of the verification condition to avoid repeated evaluation by a theorem prover of a subexpression in the verification condition that corresponds to a portion of the computer program that is common to two or more alternative paths through the program.
The purpose of a computer program verification system is to analyze a given computer program to determine whether or not it has certain desirable properties. Verification systems can also be used to analyze hardware components. A typical verification system works by generating a verification condition from a given behavioral design, and then evaluating the verification condition with a theorem prover. The verification condition is a mathematical formula. Ideally this formula is valid if and only if the original source program is free of certain kinds of errors.
The verification condition (VC) is analyzed by a theorem prover that attempts to prove the xe2x80x9ctheoremxe2x80x9d that the VC is true. When the theorem prover is unable to prove that the VC is true, it preferably provides a counter-example, which specifies at least one condition for which the VC is false. For example, if the VC is x+y greater than x, then a counter-example is yxe2x89xa60.
In general, theorem proving is difficult and may consume exorbitant computer resources. Many verification conditions are not solvable in general. Also, the size of the VC may grow exponentially with the size of the computer program from which it is derived. Another circumstance is that two mathematical formulae may be logically equivalent but one may be harder to prove than the other. Overall, significant computer resources may be expended in theorem proving, even when the computer program corresponding to the VC is not unusually complex or long.
The theory behind VC generation and theorem proving derives from that branch of mathematics known as Logic. Principles underlying VC generation also underlie the general theory of the construction of computer programs and the operation and implementation of programming languages. A theoretical treatment of VC generation in the prior-art can be found in E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, (1976); and in C. A. R. Hoare, xe2x80x9cAn Axiomatic Basis for Computer Programming,xe2x80x9d Communications of the Association for Computing Machinery, 12(10):576-83 (October 1969), both of which are hereby incorporated by reference as background information.
Several program verification systems exist in the prior art. Examples include: A Program Verifier, J. King, Ph.D. thesis, Carnegie-Mellon University (1969) in which a system, called Effigy, used Symbolic execution to generate verification conditions; L. P. Deutsch, An Interactive Program Verifier, Ph.D. thesis, Univ. Calif., Berkeley, (1973), the first program verifier to use an interactive theorem prover; D. Luckham and N. Suzuki, Automatic Program Verification V: verification-oriented rules for arrays, records and pointers, Stanford Artificial Intelligence Laboratory Memo AIM-278, (March 1976). The last of these, the Stanford Pascal Verifier, used xe2x80x9cHoare Logicxe2x80x9d to generate VC""s.
A major contribution to the intensivity of effort in applying the theorem prover is in case-splitting situations, i.e., where choices arise in the program. For example, an xe2x80x9cif . . . then . . . elsexe2x80x9d construct in a computer program provides two alternative, i.e., a pair of, conditional program execution paths, more generally called a choice. Other examples of program constructs that result in a choice are a loop with a loop termination condition, and a conditional branch. All of the aforementioned systems produced VC""s with enormous numbers of cases for programs containing a sequential composition of a significant number of alternative choice constructs.
When a computer program has the structure (S1  S2) S3 (wherein the  operator represents choice), the corresponding VC generated by methods in the prior art will normally include two instances of an expression corresponding to S3, wherein one instance is combined with an expression corresponding to S1 and another instance is combined with an expression for S2. More generally, each choice in a computer program will approximately double the size of the resulting VC because of the duplication of S3, and will thereby double the amount of work to be performed by the theorem prover to evaluate the VC. Thus, the presence of multiple choices within a computer program will typically cause the complexity of the corresponding VC to increase exponentially when using the methods of the prior art.
Therefore it is a goal of the present invention to generate a VC that is easier for the theorem prover to evaluate and which is smaller in size than the normal VC for the computer program for which the VC is being generated. None of the aforementioned program verification systems featured a solution to the problem, as addressed by the present invention.
The present invention relates to the generation of a verification condition (VC) from a computer program source code that comprises a collection of program statements.
Accordingly, the present invention involves a method of generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point, the method comprising: applying at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths.
Although a computer program can be transformed directly into a VC and take advantage of the benefits of the present invention, the overall process is facilitated by introducing an intermediate step, whereby the computer program is first converted into an intermediate form comprising xe2x80x9cguarded commands.xe2x80x9d The preferred input to the VC generator is then a set of guarded commands. In principle, a program written in any computer language can be converted this way.
In a preferred embodiment, the VC generation algorithm is the computation of a weakest precondition. In one embodiment, the weakest precondition of the set of guarded commands is computed and assignment commands (which assign values to variables) are removed from the program through use of the xe2x80x9cdynamic single assumptionxe2x80x9d technique that transforms assignment commands into program assumptions. In another embodiment, the weakest precondition is expressed in terms of strongest postconditions. The commonality between the embodiments is that labels are introduced for the values of variables at control join points and that duplication or near duplication in the VC of subexpressions derived from the expression following the control join point is avoided.
The present invention includes a method of generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point, the method comprising: when the program statements in the computer program include at least one assignment statement, transforming the at least one assignment statement into an assume command, wherein the transforming includes mapping a variable that is assigned a value by the at least one assignment statement into an expression denoting a value of the variable after the at least one assignment statement; and applying at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths. A method according to the present invention also preferably comprises passing the verification condition to a theorem prover and determining whether or not the verification condition is valid.
In a preferred embodiment, the method of the present invention additionally comprises expressing the weakest precondition operator in terms of at least one strongest postcondition operator.
Accordingly the present invention additionally comprises a computer readable medium for use in conjunction with a computer system, the computer readable medium comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising: instructions for generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point; instructions for determining when the program statements in the computer program include at least one assignment statement, and, instructions for transforming the at least one assignment statement into an assume command, wherein the transforming includes mapping a variable that is assigned a value by the at least one assignment statement into an expression denoting a value of the variable after the at least one assignment statement; and instructions for applying at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths.
The present invention also includes a computer readable medium for use in conjunction with a computer system, the computer readable medium comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising: instructions for generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point; instructions for applying at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths.
The present invention further includes a computer readable medium that comprises instructions for computing at least one precondition operator in terms of a weakest precondition operator expressed by at least one strongest postcondition operator.
The present invention additionally includes an apparatus for generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point, the apparatus comprising: a memory containing the computer program, an operating system and at least one processor configured to execute mathematical operations on the computer program, wherein the computer processor: when the program statements in the computer program include at least one assignment statement, transforms the at least one assignment statement into an assume command, and includes mapping a variable that is assigned a value by the at least one assignment statement into an expression denoting a value of the variable after the at least one assignment statement; and applies at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths.
The present invention also includes an apparatus for generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point, the apparatus comprising: a memory containing the computer program, an operating system and at least one processor configured to execute mathematical operations on the computer program, wherein the computer processor: applies at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths.
The apparatus of the present invention also includes a computer processor that computes at least one precondition operator in terms of a weakest precondition operator expressed as at least one strongest postcondition operator.